functor TypeCheck (S: TYPE_CHECK_STRUCTS): TYPE_CHECK =
struct

open S

structure A = Ast
structure I = Ir
structure T = Types2
structure E = Table
              
val error = ErrorMsg.error

local open A
in structure Id = Id
   structure Intl = Intl
   structure B = Binop
   structure L = Le
   structure Tipe = Tipe
   structure S = Structs
   structure M = Stm
   structure F = Function
   structure P = Program
end

local open I
in structure IB = Binop
   structure IL = Le
   structure IS = Structs
   structure IM = Stm
   structure IF = Function
   structure IP = Program
end
            
val tag = false
fun debugPrint s =
    if tag
    then print (String.concat [s, "\n"])
    else ()
         
structure TyCheck =
struct
fun convertTy t =
    case t
     of Tipe.Int => T.Intt
      | Tipe.Bool => T.Boolt
      | Tipe.Void => T.Voidt
      | Tipe.Struct sid => T.Name sid
      | Tipe.Pointer btype => T.Pointt (convertTy btype)
      | Tipe.Array (size, btype) => T.Arrayt (size, convertTy btype)
                                    
fun getRealTy (ty, tenv) =
    let fun get t =
            case t
             of T.Name id => (debugPrint "get real type"
                            ; getRealTy (E.looku (id, tenv), tenv))
              | _ => t
    in  get ty
    end
    
fun transBop bop = 
    let val _ = ()
    in  case bop
         of B.Plus => IB.Plus
	  | B.Minus => IB.Minus
	  | B.Times => IB.Times
	  | B.Divide => IB.Divide
	  | B.Modus => IB.Modus
	  | B.And => IB.And
	  | B.Or => IB.Or
	  | B.Eq => IB.Eq
	  | B.Ne => IB.Ne
	  | B.Gt => IB.Gt
	  | B.Ge => IB.Ge
	  | B.Lt => IB.Lt
	  | B.Le => IB.Le
    end
      
fun ckLval (tenv, venv, lval) : {ty : T.t, result : IL.lval}=
    case lval
     of L.Var (id, pos) =>
	let val {tipe, fresh} = E.looku (id, venv)
	        handle NotFound =>
	               (error pos (String.concat ["unbound variable : ", Id.toString id])
	              ; {tipe = T.Intt, fresh = Id.bogus ()})
	    val realTy = getRealTy (tipe, tenv)
	in  {ty = realTy,
	     result = IL.Var {id = fresh, ty = realTy, pos = pos}}
	end
      | L.Inptr (blval, pos) =>
	let val {ty = ty1, result = result1} =
	        ckLval (tenv, venv, blval)
	    val ty =
	        case ty1
	         of T.Pointt t => getRealTy (t, tenv)
	          | _ => (error pos ("pointer type required"); T.Intt)
	in  {ty = ty, result = IL.Ptr (IL.Sharp ty, result1, pos)}
	end
      | L.Inarray (blval, exp, pos) =>
	let val {ty = tyl, result = resultl} = ckLval (tenv, venv, blval)
	    val {ty = tye, result = resulte} = ckExp (tenv, venv, exp)
	    fun getSizeAndTy t =
	        case tyl
	         of T.Arrayt (i, ty) =>
	            let val realTy = getRealTy (ty, tenv)
	            in  if T.equals (tye, T.Intt)
                        then (i, realTy)
	                else (error pos ("int type expected"); (i, realTy))
	            end
	          | _ => (error pos ("array type expected"); (Intl.fromInt ~1, tye))
	    val (size, realty) = getSizeAndTy tyl
	in  {ty = realty, result = IL.Inarray {lval = resultl, exp = resulte, length = size, ty = tyl, pos = pos}}
	end
      | L.Instruct (slval, fname, pos) =>
	let val {ty = ty, result = result} = ckLval (tenv, venv, slval)
	    fun ck ty =
	        case ty
	         of T.Structt (l, u) =>
	            let fun loop lx =
	                    case lx
	                     of [] => (error pos ("cannot get the field type ")
	                             ; (T.Intt, Intl.fromInt (~1)))
	                      | {id, offSet, ty} :: xs =>
	                        if Id.equals (fname, id)
	                        then (ty, offSet)
	                        else loop xs
	            in  loop l
	            end
	          | _ => (error pos ("struct type expected")
	                ; (T.Intt, Intl.fromInt (~1)))
	    val (tyy, offSet) = ck ty
	in  {ty = tyy, result = IL.Instruct {lval = result, id = fname, offSet = offSet, pos = pos}}
	end
      | L.Ptstruct (slval, fname, pos) =>
	ckLval (tenv, venv, L.Instruct (L.Inptr (slval, pos), fname, pos))
      | L.Ptstruct2 (slval, fname, id2, pos) =>
        ckLval (tenv, venv, L.Instruct (L.Inptr (slval, pos), fname, pos))
        
and transLvals (tenv, venv, l, pos) = 
    case l
     of [] => []
      | x :: xs => 
    	let val {ty, result} = ckLval (tenv, venv, x)
    	    val _ = if T.isPtTy ty
    	            then ()
    	            else error pos "pointer type wanted" 
    	in  (result :: transLvals (tenv, venv, xs, pos))
    	end
        
and transLvalss (tenv, venv, l, pos) =
    case l
     of [] => []
      | x :: xs => 
    	transLvals (tenv, venv, x, pos) :: transLvalss (tenv, venv, xs, pos)
    	
and ckBop (bop, t1, t2, pos) =
    let fun ck (t1, t2, t) =
            if T.equals (t1, t2) andalso T.equals (t1, t)
            then t1
            else (error pos "type mismatch\n"; T.Intt)
        fun ck2 (t1, t2) =
            if T.equals (t1, t2)
            then if T.equals (t1, T.Intt) orelse T.isPtTy t1
                 then T.Boolt
                 else (error pos "type mismatch\n"; T.Intt)
            else (error pos "type mismatch\n"; T.Intt)
        fun ck3 (t1, t2) =
            if T.equals (t1, t2) andalso T.equals (t1, T.Intt)
            then T.Boolt
            else (error pos "type mismatch\n"; T.Boolt)
    in  case bop
         of B.Plus => ck (t1, t2, T.Intt)
	  | B.Minus => ck (t1, t2, T.Intt)
	  | B.Times => ck (t1, t2, T.Intt)
	  | B.Divide => ck (t1, t2, T.Intt)
	  | B.Modus => ck (t1, t2, T.Intt)
	  | B.And => ck (t1, t2, T.Boolt)
	  | B.Or => ck (t1, t2, T.Boolt)
	  | B.Eq => ck2 (t1, t2)
	  | B.Ne => ck2 (t1, t2)
	  | B.Gt => ck3 (t1, t2)
	  | B.Ge => ck3 (t1, t2)
	  | B.Lt => ck3 (t1, t2)
	  | B.Le => ck3 (t1, t2)
    end
    
and ckExp (tenv, venv, exp) : {ty : T.t, result : IL.exp}=
    case exp
     of L.Expvoid =>
        {ty = T.Voidt, result = IL.Expvoid}
      | L.IntNum i =>
	{ty = T.Intt, result = IL.IntNum i}
      | L.BinopExp (e1, bop, e2, pos) =>
	let val {ty = ty1, result = result1} = ckExp (tenv, venv, e1)
	    val {ty = ty2, result = result2} = ckExp (tenv, venv, e2)
	    val t = ckBop (bop, ty1, ty2, pos)
	in  {ty = t, 
	     result = IL.BinopExp {left = result1,
	                           bop = transBop bop, 
	                           right = result2, 
	                           ty = t, 
	                           pos = pos}}
	end
      | L.NotExp (e, pos) =>
	let val {ty = ty, result = result} = ckExp (tenv, venv, e)
	    val ty = if T.equals (ty, T.Boolt)
                     then (error pos (": unary operation error! "); T.Intt)
	             else ty
	in  {ty = ty, result = IL.NotExp (result, pos)}
	end
      | L.Lval lval =>
	let val {ty = ty, result = result} = ckLval (tenv, venv, lval)
	in  {ty = ty, result = IL.Lval {lval = result, ty = ty}}
	end
          
fun ckStm (tenv, venv, stm, fname) =
    case stm
     of M.AsnExp (lval, e, pos) =>
	let val {ty = tyl, result = resultl} = ckLval (tenv, venv, lval)
	    val {ty = tye, result = resulte} = ckExp (tenv, venv, e)
	    val _ = debugPrint "checking asn exp"
	    val _ = if T.equals (tyl, tye)
                    then ()
                    else (debugPrint ((T.toString tyl)^"\n");
                          debugPrint ((T.toString tye)^ "\n");
                          error pos "assignment type mismatch")
	in  {result = IM.AsnExp {lval = resultl, exp = resulte, ty = tyl, pos = pos}}
	end
      | M.AsnCall (lval, fname, paralist, pos) =>
	let val paras = List.map (fn x => (ckExp (tenv, venv, x))) paralist
	      val paraTys = List.map #ty paras
	      val paraResult = List.map #result paras
	      val realParaTys = T.Product paraTys
	      val {ty = tyl, result = resultl} = ckLval (tenv, venv, lval)
	      val fTy = getRealTy (#tipe (E.looku (fname, venv)), tenv)
	                handle NotFound =>
	                (error pos (String.concat ["unbound function : ",
                                                   Id.toString fname])
                         ; T.Intt)
              val retTy = case fTy
	       of T.Funct (argTy, retTy) =>
	          let val realArgTy = getRealTy (argTy, tenv)
	              val realRetTy = getRealTy (retTy, tenv)
	          in
	          if T.equals (realArgTy, realParaTys)
	          then if T.equals (realRetTy, tyl)
                       then realRetTy
	               else (error pos (String.concat ["function\
                        \ call assignment types mismatch : ",
                                                      Id.toString fname])
                                                      ; T.Intt)
	          else (error pos (String.concat ["function\
                   \ parameters types mismatch : ",
                                                 Id.toString fname])
                                                 ; T.Intt)
                  end
	        | _ => (error pos (String.concat ["function\
                 \ type expected : ",
                                                 Id.toString fname]);
                                                 T.Intt)
	  in  {result = IM.AsnCall {lval = resultl, fid = fname, ty = retTy, exps = paraResult, pos = pos}}
	  end
      | M.If (cond, s1, s2, pos) =>
	let val {ty = tye, result = resulte} = ckExp (tenv, venv, cond)
	    val {result = rs1} = ckStms (tenv, venv, s1, fname)
	    val {result = rs2} = ckStms (tenv, venv, s2, fname)
	    val _ = if T.equals (tye, T.Boolt)
	            then ()
	            else error pos "if condition type should be bool"
	in  {result = IM.If (resulte, rs1, rs2, pos)}
	end
      | M.While {condition, body, pos} =>
	let val {ty = tye, result = resulte} = ckExp (tenv, venv, condition)
	    val {ty = tyi, result = resulti} = ckExp (tenv, venv, invariant)
	    val _ = debugPrint "the value of resulte is:\n"
	    val _ = debugPrint (IL.expToString resulte)
	    val _ = debugPrint "the value of resulti is:\n"
	    val _ = debugPrint (IL.expToString resulti)	      
	    val {result = rbody} = ckStms (tenv, venv, body, fname)
	    val _ = if T.equals (tye, T.Boolt)
	            then if T.equals (tyi, T.Boolt)
	                 then ()
	                 else error pos "invariant type error"
	            else error pos "condition type error"
	in  {result = IM.While {condition = resulte, invariant = resulti, body = rbody, pos = pos}}
	end
      | M.Return (e, pos) =>
	let val {ty = ty, result = result} = ckExp (tenv, venv, e)
	    val {tipe = fty, fresh} = E.looku (fname, venv)
	        handle NotFound => (error pos (String.concat
                                                   ["unbound function: ",
                                                    Id.toString fname])
                                  ; {tipe = T.Intt, fresh = Id.bogus ()})
	    val rettype = case fty
	                   of T.Funct (_, ret) => ret
	                    | _ => (error pos (String.concat
                                                   ["function type expected: ",
                                                    Id.toString fname])
                                  ; T.Intt)
            val _ = if T.equals (ty, rettype)
	            then ()
	            else error pos "return type error"
	in  {result = IM.Return {exp = result, fty = rettype, pos = pos}}
	end
      | M.Call (f, paras, pos) =>
	let val parasNew = List.map (fn a => ckExp (tenv, venv, a)) paras
	    val tys = List.map #ty parasNew
	    val tys = T.Product tys
	    val results = List.map #result parasNew
	    val {tipe = fty, fresh = ffff} = E.looku (f, venv)
	        handle NotFound => (error pos (String.concat
                                                   ["unbound function: ",
                                                    Id.toString fname])
                                  ; {tipe = T.Intt, fresh = Id.bogus ()})
	    val argsty = case fty
	                  of T.Funct (args, _) => args
	                   | _ => (error pos (String.concat
                                                  ["function type expected: ",
                                                   Id.toString fname])
                                 ; T.Intt)
            val _ = if T.equals (tys, argsty)
	            then ()
	            else error pos (String.concat ["function argument type error\n",
	                                           "wants   : ", T.toString argsty, "\n",
	                                           "but got : ", T.toString tys, "\n"])
	in  {result = IM.Call (f, results, pos)}
	end
        
and ckStms (tenv, venv, stms, fname) =
    let val ss = List.map (fn x =>
                              #result (ckStm (tenv, venv, x, fname)))
                          stms
    in {result = ss}
    end
    
fun ckGvarDec (tenv, venv, vars, pos) =
    let fun ck ({id, ty}, venv) =
            let val ty1 = getRealTy (convertTy ty, tenv)
                val fresh = Id.new ()
            in  (E.enteru (id, {tipe = ty1, fresh = fresh}, venv), {id = fresh, ty = ty1})
                handle Duplicate =>
                       (error pos (String.concat ["duplicate variable definition: ",
                                                  Id.toString id,
                                                  "\n"])
	              ; (venv, {id = id, ty = ty1}))
            end
        fun loop (l, venv) =
            case l
             of [] => (venv, [])
              | x :: xs =>
                let val (venv, new) = ck (x, venv)
                    val (venv', new') = loop (xs, venv)
                in  (venv', new :: new')
                end                 
        val res = loop (vars, venv)
    in  res
    end
    
fun ckStructDec (tenv, structId, fields) =
    let fun validNameTy ty =
            case ty
             of T.Name _ => false
              | _ => true
        fun ck (l, i) =
            case l
             of [] => []
              | {id, ty} :: xs =>
                let val ty1 = convertTy ty
                    val _ = if validNameTy ty1
                            then ()
                            else (error 0 "invalid reference")
                in  {id = id, offSet = Intl.fromInt i, ty = ty1} :: (ck (xs, i+1))
                end
        val ty2 = T.Structt (ck (fields, 0), ref ())
    in  E.enter (structId, ty2, tenv)
    end
    
fun ckStruct (tenv, s) =
    case s
     of S.T {name,
             fields,
             pos} =>
        ckStructDec (tenv, name, fields)
        
fun ckFunction (tenv, venv, f) =
    case f
     of F.T {name,
             rettype,
             args,
             stm} =>
        let val (venv1, newArgs) = ckGvarDec (tenv, venv, args, pos)
              val (venv1, newLocals) = ckGvarDec (tenv, venv1, locals, pos)
              val {result = resultPre, ...} = ckExp (tenv, venv1, pre)
              val {result = resultPost, ...} = ckExp (tenv, venv1, post)
              val {result} = ckStms (tenv, venv1, stm, name)
          in  IF.T {name = name,
                    rettype = getRealTy (convertTy (rettype), tenv),
                    args = newArgs,
                    locals = newLocals,
                    stm = result,
                    pre = resultPre,
                    post = resultPost,
                    pos = pos}
          end

  fun ckProg (tenv, venv, ast) =
      case ast
       of P.T {structs,
               gvars,
               funcs,
               pos} =>
          let val tenv1 = List.foldl (fn (a, b) => ckStruct (b, a)) tenv structs
              val _ = debugPrint "the new tenv is:"
              val _ = debugPrint (E.tenvToString tenv1)
              val (venv2, newGvars) = ckGvarDec (tenv1, venv, gvars, pos)
              val funcs = List.map (fn x =>
                                  ckFunction (tenv1, venv2, x)) funcs
          in  IP.T {structs = [],
                    gvars = newGvars,
                    funcs = funcs,
                    pos = pos}
          end

  fun collectStruct (tenv, s) =
      case s
       of S.T {name,
               fields,
               pos} =>
          E.enteru (name, T.Name name, tenv)
          handle Duplicate => (error pos (String.concat
                                          ["duplicate struct definition: ",
                                           Id.toString name,
                                           "\n"])
                               ; tenv)

  fun collectFun (venv, f) =
      case f
       of F.T {name,
               rettype,
               args,
               locals,
               stm} =>
          let val argt = T.Product (List.map (convertTy o #ty) args)
	      val funt = T.Funct (argt, convertTy rettype)
	      val venv1 = E.enteru (name, {tipe = funt, fresh = name}, venv)
	                  handle Dupplicate =>
	                  (error pos (String.concat
                                      ["rebounded function name: ",
                                       Id.toString name,
                                       "\n"])
	                  ; venv)
	  in  venv1
	  end

  fun collectInfo (tenv, venv, ast) =
      case ast
       of P.T {structs,
               gvars,
               funcs,
               pos} =>
          let val tenv1 = List.foldl (fn (a, b) => collectStruct (b, a))
            tenv
            structs
              val venv1 = List.foldl (fn (a, b) => collectFun (b, a))
                venv
                funcs
          in  (tenv1, venv1)
          end

  fun ckTop ast =
      let val tenv = E.baseTenv ()
	  val venv = E.baseVenv ()
	  val (tenv1, venv1) = collectInfo (tenv, venv, ast)
	  val _ = debugPrint "the initial tenv is:"
	  val _ = debugPrint (E.tenvToString tenv1)
	  val _ = debugPrint "translate to program starting"
	  val ir = ckProg (tenv1, venv1, ast)
	  val _ = debugPrint "translate to program finished"
      in  ir
      end
end

structure RetCheck =
struct

  fun ckStm stm =
      case stm
       of M.AsnExp (lval, e, pos) => false
	| M.AsnCall (lval, fname, paralist, pos) => false
	| M.If (cond, s1, s2, pos) => (ckStms s1) andalso (ckStms s2)
	| M.While _ => false
	| M.Return (e, pos) => true
	| M.Call (fname, paras, pos) => false

  and ckStms stms =
      case stms
       of [] => false
        | x :: xs => (ckStm x) orelse (ckStms xs)

  fun ckFunction f =
      case f
       of F.T {name,
               rettype,
               args,
               locals,
               stm} =>
         if ckStms stm
         then ()
         else error pos "no return, fall through\n"

  fun ckProgram p =
      case p
       of P.T {structs,
               gvars,
               funcs,
               pos} =>
          List.app ckFunction funcs

  fun ckTop ast =
      if !Control.doSkipReturn
      then ()
      else ckProgram ast
end


end
